p:finite-prob-space. 0  p-outcome(p) 

latex

Definitions	A, b, null(as), #$n, p-outcome(p), , P  Q, decidable(P), P  Q, left + right, isect(A; x.B(x)), void, finite-prob-space, {x:A| B(x)} , P  Q, subtype(S; T), x:A. B(x), x:AB(x), rationals, t  T, type List, top, int_seg(i; j), lelt(i; j; k), x:A  B(x), A  B, a < b, , False, True, ge(i; j), n + m, ||as||, [], cons(car; cdr)
Lemmas	fps-not-null, length wf1, non neg length, nat wf, length wf nat, le wf, null wf3, rationals wf, top wf, assert wf, decidable assert, decidable not, finite-prob-space wf